1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
/*!
An abstract syntax tree for the textual representation of `isotope`
*/
use super::*;

/// An `isotope` statement
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub enum Stmt {
    /// A `let`-statement
    Let(Let),
    /// A `join`-statmenet
    Join(Join),
}

/// An `isotope` expression
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub enum Expr {
    // Basic terms:
    /// An identifier
    Ident(SmolStr),
    /// A variable index
    Var(u32),
    /// A function application
    App(App),
    /// A lambda function
    Lambda(Lambda),
    /// A dependent function type
    Pi(Pi),
    /// A typing universe
    Universe(Universe),

    // Primitive terms:
    /// An enumeration
    Enum(Enum),
    /// A variant
    Variant(SmolStr),
    /// A boolean value
    Boolean(bool),
    /// A natural number
    Natural(BigUint),
    /// The type of booleans
    Bool,
    /// The unit type
    Unit,

    // Primitive operations:
    /// A case expression
    Case(Case),

    // Inference:
    /// An annotated term
    Annotated(Annotated),
    /// A scope
    Scope(Scope),
}

/// A `let` statement
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Let {
    /// The identifier being assigned
    pub ident: Option<String>,
    /// The type of this identifier, if specified
    pub ty: Option<Arc<Expr>>,
    /// The value the identifier is being assigned
    pub value: Arc<Expr>,
}

/// A `join` statement
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Join {
    /// The reduction types allowed
    pub form: Form,
    /// The source expression
    pub source: Arc<Expr>,
    /// The work limit
    pub work_limit: Option<u64>,
    /// The target expression, if any
    pub target: Option<Arc<Expr>>,
}

/// A function application
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct App(pub SmallVec<[Arc<Expr>; 2]>);

/// A lambda function
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Lambda {
    /// The parameter name of this lambda function, if any
    pub param_name: Option<SmolStr>,
    /// The parameter type of this lambda function, if any
    pub param_ty: Option<Arc<Expr>>,
    /// The result of this lambda function
    pub result: Arc<Expr>,
}

/// A dependent function type
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Pi {
    /// The parameter name of this dependent function type, if any
    pub param_name: Option<Option<SmolStr>>,
    /// The parameter type of this dependent function type
    pub param_ty: Arc<Expr>,
    /// The result of this lambda function
    pub result: Arc<Expr>,
}

/// A typing universe
#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
pub struct Universe(u32);

impl Universe {
    /// Construct a universe from a level and whether it is a variable
    #[inline]
    pub fn try_new(level: u32, is_var: bool) -> Result<Universe, ()> {
        if is_var {
            Universe::try_var(level)
        } else {
            Universe::try_const(level)
        }
    }
    /// Attempt to construct a constant universe from it's level
    #[inline]
    pub fn try_const(level: u32) -> Result<Universe, ()> {
        Ok(Universe(level.checked_mul(2).ok_or(())?))
    }
    /// Attempt to construct a universe variable from it's level
    #[inline]
    pub fn try_var(level: u32) -> Result<Universe, ()> {
        Ok(Universe(
            level.checked_mul(2).ok_or(())?.checked_add(1).ok_or(())?,
        ))
    }
    /// Get the level of this universe
    #[inline]
    pub fn level(self) -> u32 {
        self.0 / 2
    }
    /// Get whether this universe is a variable
    #[inline]
    pub fn is_var(self) -> bool {
        self.0 % 2 == 1
    }
}

/// An enumeration
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Enum(pub Vec<SmolStr>);

/// A case expression
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Case(pub Vec<Branch>);

/// A branch of a case expression
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Branch {
    /// The pattern
    pub pattern: Arc<Expr>,
    /// The result
    pub result: Arc<Expr>,
}

/// An annotated term
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Annotated {
    /// The underlying term
    pub term: Arc<Expr>,
    /// The type this term is assigned
    //TODO: more general annotations?
    pub ty: Arc<Expr>,
}

/// A scope
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct Scope {
    /// The statements in this scope
    pub stmts: Vec<Stmt>,
    /// The result value of this scope
    pub result: Arc<Expr>,
}

/// A reduction form
#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
pub enum Form {
    /// No reductions: check only for equality
    Null,
    /// Head reductions only
    Head,
    /// Beta reductions
    Beta,
    /// Eta reductions
    Eta,
    /// Beta and eta reductions
    BetaEta,
}

impl Form {
    /// Whether to perform head reductions
    pub const fn head(self) -> bool {
        use Form::*;
        matches!(self, Head | Beta | BetaEta)
    }
    /// Whether to perform sub reductions
    pub const fn sub(self) -> bool {
        use Form::*;
        matches!(self, Eta | Beta | BetaEta)
    }
    /// Whether to perform eta reductions
    pub const fn eta(self) -> bool {
        use Form::*;
        matches!(self, Eta | BetaEta)
    }
}